↳ ITRS
↳ ITRStoQTRSProof
z
sqrtAcc(x, y) → condAcc(||(>=@z(*@z(y, y), x), <@z(y, 0@z)), x, y)
sqrt(x) → sqrtAcc(x, 0@z)
condAcc(FALSE, x, y) → sqrtAcc(x, +@z(y, 1@z))
condAcc(TRUE, x, y) → y
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(FALSE, x0, x1)
condAcc(TRUE, x0, x1)
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(x, y) → CONDACC(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
SQRTACC(x, y) → OR(greatereq_int(mult_int(y, y), x), less_int(y, pos(0)))
SQRTACC(x, y) → GREATEREQ_INT(mult_int(y, y), x)
SQRTACC(x, y) → MULT_INT(y, y)
SQRTACC(x, y) → LESS_INT(y, pos(0))
SQRT(x) → SQRTACC(x, pos(0))
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
CONDACC(false, x, y) → PLUS_INT(pos(s(0)), y)
GREATEREQ_INT(pos(s(x)), pos(s(y))) → GREATEREQ_INT(pos(x), pos(y))
GREATEREQ_INT(neg(s(x)), neg(s(y))) → GREATEREQ_INT(neg(x), neg(y))
MULT_INT(pos(x), pos(y)) → MULT_NAT(x, y)
MULT_INT(pos(x), neg(y)) → MULT_NAT(x, y)
MULT_INT(neg(x), pos(y)) → MULT_NAT(x, y)
MULT_INT(neg(x), neg(y)) → MULT_NAT(x, y)
MULT_NAT(s(x), s(y)) → PLUS_NAT(mult_nat(x, s(y)), s(y))
MULT_NAT(s(x), s(y)) → MULT_NAT(x, s(y))
PLUS_NAT(s(x), y) → PLUS_NAT(x, y)
LESS_INT(pos(s(x)), pos(s(y))) → LESS_INT(pos(x), pos(y))
LESS_INT(neg(s(x)), neg(s(y))) → LESS_INT(neg(x), neg(y))
PLUS_INT(pos(x), neg(y)) → MINUS_NAT(x, y)
PLUS_INT(neg(x), pos(y)) → MINUS_NAT(y, x)
PLUS_INT(neg(x), neg(y)) → PLUS_NAT(x, y)
PLUS_INT(pos(x), pos(y)) → PLUS_NAT(x, y)
MINUS_NAT(s(x), s(y)) → MINUS_NAT(x, y)
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
SQRTACC(x, y) → CONDACC(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
SQRTACC(x, y) → OR(greatereq_int(mult_int(y, y), x), less_int(y, pos(0)))
SQRTACC(x, y) → GREATEREQ_INT(mult_int(y, y), x)
SQRTACC(x, y) → MULT_INT(y, y)
SQRTACC(x, y) → LESS_INT(y, pos(0))
SQRT(x) → SQRTACC(x, pos(0))
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
CONDACC(false, x, y) → PLUS_INT(pos(s(0)), y)
GREATEREQ_INT(pos(s(x)), pos(s(y))) → GREATEREQ_INT(pos(x), pos(y))
GREATEREQ_INT(neg(s(x)), neg(s(y))) → GREATEREQ_INT(neg(x), neg(y))
MULT_INT(pos(x), pos(y)) → MULT_NAT(x, y)
MULT_INT(pos(x), neg(y)) → MULT_NAT(x, y)
MULT_INT(neg(x), pos(y)) → MULT_NAT(x, y)
MULT_INT(neg(x), neg(y)) → MULT_NAT(x, y)
MULT_NAT(s(x), s(y)) → PLUS_NAT(mult_nat(x, s(y)), s(y))
MULT_NAT(s(x), s(y)) → MULT_NAT(x, s(y))
PLUS_NAT(s(x), y) → PLUS_NAT(x, y)
LESS_INT(pos(s(x)), pos(s(y))) → LESS_INT(pos(x), pos(y))
LESS_INT(neg(s(x)), neg(s(y))) → LESS_INT(neg(x), neg(y))
PLUS_INT(pos(x), neg(y)) → MINUS_NAT(x, y)
PLUS_INT(neg(x), pos(y)) → MINUS_NAT(y, x)
PLUS_INT(neg(x), neg(y)) → PLUS_NAT(x, y)
PLUS_INT(pos(x), pos(y)) → PLUS_NAT(x, y)
MINUS_NAT(s(x), s(y)) → MINUS_NAT(x, y)
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
MINUS_NAT(s(x), s(y)) → MINUS_NAT(x, y)
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
MINUS_NAT(s(x), s(y)) → MINUS_NAT(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
MINUS_NAT(s(x), s(y)) → MINUS_NAT(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LESS_INT(neg(s(x)), neg(s(y))) → LESS_INT(neg(x), neg(y))
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LESS_INT(neg(s(x)), neg(s(y))) → LESS_INT(neg(x), neg(y))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LESS_INT(neg(s(x)), neg(s(y))) → LESS_INT(neg(x), neg(y))
No rules are removed from R.
LESS_INT(neg(s(x)), neg(s(y))) → LESS_INT(neg(x), neg(y))
POL(LESS_INT(x1, x2)) = 2·x1 + x2
POL(neg(x1)) = x1
POL(s(x1)) = 2·x1
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LESS_INT(pos(s(x)), pos(s(y))) → LESS_INT(pos(x), pos(y))
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LESS_INT(pos(s(x)), pos(s(y))) → LESS_INT(pos(x), pos(y))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LESS_INT(pos(s(x)), pos(s(y))) → LESS_INT(pos(x), pos(y))
No rules are removed from R.
LESS_INT(pos(s(x)), pos(s(y))) → LESS_INT(pos(x), pos(y))
POL(LESS_INT(x1, x2)) = 2·x1 + x2
POL(pos(x1)) = x1
POL(s(x1)) = 2·x1
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PLUS_NAT(s(x), y) → PLUS_NAT(x, y)
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PLUS_NAT(s(x), y) → PLUS_NAT(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PLUS_NAT(s(x), y) → PLUS_NAT(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
MULT_NAT(s(x), s(y)) → MULT_NAT(x, s(y))
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
MULT_NAT(s(x), s(y)) → MULT_NAT(x, s(y))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
MULT_NAT(s(x), s(y)) → MULT_NAT(x, s(y))
From the DPs we obtained the following set of size-change graphs:
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
GREATEREQ_INT(neg(s(x)), neg(s(y))) → GREATEREQ_INT(neg(x), neg(y))
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
GREATEREQ_INT(neg(s(x)), neg(s(y))) → GREATEREQ_INT(neg(x), neg(y))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ QDP
GREATEREQ_INT(neg(s(x)), neg(s(y))) → GREATEREQ_INT(neg(x), neg(y))
No rules are removed from R.
GREATEREQ_INT(neg(s(x)), neg(s(y))) → GREATEREQ_INT(neg(x), neg(y))
POL(GREATEREQ_INT(x1, x2)) = 2·x1 + x2
POL(neg(x1)) = x1
POL(s(x1)) = 2·x1
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
GREATEREQ_INT(pos(s(x)), pos(s(y))) → GREATEREQ_INT(pos(x), pos(y))
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
GREATEREQ_INT(pos(s(x)), pos(s(y))) → GREATEREQ_INT(pos(x), pos(y))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
GREATEREQ_INT(pos(s(x)), pos(s(y))) → GREATEREQ_INT(pos(x), pos(y))
No rules are removed from R.
GREATEREQ_INT(pos(s(x)), pos(s(y))) → GREATEREQ_INT(pos(x), pos(y))
POL(GREATEREQ_INT(x1, x2)) = 2·x1 + x2
POL(pos(x1)) = x1
POL(s(x1)) = 2·x1
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ UsableRulesReductionPairsProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(x, y) → CONDACC(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrtAcc(x, y) → condAcc(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
sqrt(x) → sqrtAcc(x, pos(0))
condAcc(false, x, y) → sqrtAcc(x, plus_int(pos(s(0)), y))
condAcc(true, x, y) → y
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(pos(x), neg(y)) → neg(mult_nat(x, y))
mult_int(neg(x), pos(y)) → neg(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
less_int(pos(0), pos(0)) → false
less_int(pos(0), neg(0)) → false
less_int(neg(0), pos(0)) → false
less_int(neg(0), neg(0)) → false
less_int(pos(0), pos(s(y))) → true
less_int(neg(0), pos(s(y))) → true
less_int(pos(0), neg(s(y))) → false
less_int(neg(0), neg(s(y))) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
less_int(pos(s(x)), neg(0)) → false
less_int(neg(s(x)), neg(0)) → true
less_int(pos(s(x)), neg(s(y))) → false
less_int(neg(s(x)), pos(s(y))) → true
less_int(pos(s(x)), pos(s(y))) → less_int(pos(x), pos(y))
less_int(neg(s(x)), neg(s(y))) → less_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(x, y) → CONDACC(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
less_int(pos(0), pos(0)) → false
less_int(neg(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
sqrtAcc(x0, x1)
sqrt(x0)
condAcc(false, x0, x1)
condAcc(true, x0, x1)
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(x, y) → CONDACC(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
less_int(pos(0), pos(0)) → false
less_int(neg(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ QDP
↳ RemovalProof
↳ Narrowing
CONDACC(false, x, y, x_removed) → SQRTACC(x, plus_int(x_removed, y), x_removed)
SQRTACC(x, y, x_removed) → CONDACC(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y, x_removed)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
less_int(pos(0), pos(0)) → false
less_int(neg(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ QDP
↳ Narrowing
CONDACC(false, x, y, x_removed) → SQRTACC(x, plus_int(x_removed, y), x_removed)
SQRTACC(x, y, x_removed) → CONDACC(or(greatereq_int(mult_int(y, y), x), less_int(y, pos(0))), x, y, x_removed)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
less_int(pos(0), pos(0)) → false
less_int(neg(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(mult_int(neg(0), neg(0)), y0), false), y0, neg(0))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(mult_int(neg(s(x0)), neg(s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(mult_int(pos(0), pos(0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(mult_int(pos(s(x0)), pos(s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(mult_int(neg(0), neg(0)), y0), false), y0, neg(0))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(mult_int(neg(s(x0)), neg(s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(mult_int(pos(0), pos(0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(mult_int(pos(s(x0)), pos(s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
less_int(pos(0), pos(0)) → false
less_int(neg(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, neg(0))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(mult_int(neg(s(x0)), neg(s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(mult_int(pos(0), pos(0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(mult_int(pos(s(x0)), pos(s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, neg(0))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
less_int(pos(0), pos(0)) → false
less_int(neg(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), true), y0, neg(s(x0)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(mult_int(pos(0), pos(0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(mult_int(pos(s(x0)), pos(s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), true), y0, neg(s(x0)))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
mult_int(neg(x), neg(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
less_int(pos(0), pos(0)) → false
less_int(neg(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(false, true) → true
or(true, false) → true
or(true, true) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(mult_int(pos(0), pos(0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(mult_int(pos(s(x0)), pos(s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), true), y0, neg(s(x0)))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, pos(0))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(mult_int(pos(s(x0)), pos(s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, pos(0))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), false), y0, pos(s(x0)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), false), y0, pos(s(x0)))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mult_int(pos(x), pos(y)) → pos(mult_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
mult_nat(s(x), 0) → 0
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), false), y0, pos(s(x0)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
mult_int(pos(x0), pos(x1))
mult_int(pos(x0), neg(x1))
mult_int(neg(x0), pos(x1))
mult_int(neg(x0), neg(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), false), y0, pos(s(x0)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, neg(0))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, neg(0))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(mult_nat(0, 0)), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, pos(0))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(mult_nat(s(x0), s(x0))), y0), false), y0, pos(s(x0)))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, pos(0))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
CONDACC(false, x, y) → SQRTACC(x, plus_int(pos(s(0)), y))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
CONDACC(false, y0, neg(x1)) → SQRTACC(y0, minus_nat(s(0), x1))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(plus_nat(s(0), x1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
SQRTACC(y0, neg(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, neg(0))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, neg(x1)) → SQRTACC(y0, minus_nat(s(0), x1))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(plus_nat(s(0), x1)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(plus_nat(s(0), x1)))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(plus_nat(s(0), x1)))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
or(false, false) → false
or(true, false) → true
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(plus_nat(s(0), x1)))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
or(false, false) → false
or(true, false) → true
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(plus_nat(0, x1))))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(0)) → CONDACC(or(greatereq_int(pos(0), y0), false), y0, pos(0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(plus_nat(0, x1))))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
or(false, false) → false
or(true, false) → true
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(plus_nat(0, x1))))
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
or(false, false) → false
or(true, false) → true
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(x1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
SQRTACC(y0, pos(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(pos(x0), pos(0))), y0, pos(x0))
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(x1)))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
or(false, false) → false
or(true, false) → true
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
SQRTACC(z0, pos(s(z1))) → CONDACC(or(greatereq_int(pos(mult_nat(s(z1), s(z1))), z0), less_int(pos(s(z1)), pos(0))), z0, pos(s(z1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(x1)))
SQRTACC(z0, pos(s(z1))) → CONDACC(or(greatereq_int(pos(mult_nat(s(z1), s(z1))), z0), less_int(pos(s(z1)), pos(0))), z0, pos(s(z1)))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
or(false, false) → false
or(true, false) → true
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(x1)))
SQRTACC(z0, pos(s(z1))) → CONDACC(or(greatereq_int(pos(mult_nat(s(z1), s(z1))), z0), less_int(pos(s(z1)), pos(0))), z0, pos(s(z1)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
SQRTACC(z0, pos(s(z1))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(z1, s(z1)), s(z1))), z0), less_int(pos(s(z1)), pos(0))), z0, pos(s(z1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(x1)))
SQRTACC(z0, pos(s(z1))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(z1, s(z1)), s(z1))), z0), less_int(pos(s(z1)), pos(0))), z0, pos(s(z1)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
SQRTACC(z0, pos(s(z1))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(z1, s(z1)), s(z1))), z0), false), z0, pos(s(z1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(x1)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(x1)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, y0, pos(x1)) → SQRTACC(y0, pos(s(x1)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
CONDACC(false, z0, pos(s(z1))) → SQRTACC(z0, pos(s(s(z1))))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
SQRTACC(y0, pos(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), false), y0, pos(s(x0)))
CONDACC(false, z0, pos(s(z1))) → SQRTACC(z0, pos(s(s(z1))))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
SQRTACC(z0, pos(s(s(z1)))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(s(z1), s(s(z1))), s(s(z1)))), z0), false), z0, pos(s(s(z1))))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
CONDACC(false, z0, pos(s(z1))) → SQRTACC(z0, pos(s(s(z1))))
SQRTACC(z0, pos(s(s(z1)))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(s(z1), s(s(z1))), s(s(z1)))), z0), false), z0, pos(s(s(z1))))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
SQRTACC(z0, pos(s(s(z1)))) → CONDACC(or(greatereq_int(pos(plus_nat(plus_nat(mult_nat(z1, s(s(z1))), s(s(z1))), s(s(z1)))), z0), false), z0, pos(s(s(z1))))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
CONDACC(false, z0, pos(s(z1))) → SQRTACC(z0, pos(s(s(z1))))
SQRTACC(z0, pos(s(s(z1)))) → CONDACC(or(greatereq_int(pos(plus_nat(plus_nat(mult_nat(z1, s(s(z1))), s(s(z1))), s(s(z1)))), z0), false), z0, pos(s(s(z1))))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
CONDACC(false, z0, pos(s(s(z1)))) → SQRTACC(z0, pos(s(s(s(z1)))))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
SQRTACC(z0, pos(s(s(z1)))) → CONDACC(or(greatereq_int(pos(plus_nat(plus_nat(mult_nat(z1, s(s(z1))), s(s(z1))), s(s(z1)))), z0), false), z0, pos(s(s(z1))))
CONDACC(false, z0, pos(s(s(z1)))) → SQRTACC(z0, pos(s(s(s(z1)))))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
SQRTACC(z0, pos(s(s(s(z1))))) → CONDACC(or(greatereq_int(pos(plus_nat(plus_nat(mult_nat(s(z1), s(s(s(z1)))), s(s(s(z1)))), s(s(s(z1))))), z0), false), z0, pos(s(s(s(z1)))))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
CONDACC(false, z0, pos(s(s(z1)))) → SQRTACC(z0, pos(s(s(s(z1)))))
SQRTACC(z0, pos(s(s(s(z1))))) → CONDACC(or(greatereq_int(pos(plus_nat(plus_nat(mult_nat(s(z1), s(s(s(z1)))), s(s(s(z1)))), s(s(s(z1))))), z0), false), z0, pos(s(s(s(z1)))))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
SQRTACC(z0, pos(s(s(s(z1))))) → CONDACC(or(greatereq_int(pos(plus_nat(plus_nat(plus_nat(mult_nat(z1, s(s(s(z1)))), s(s(s(z1)))), s(s(s(z1)))), s(s(s(z1))))), z0), false), z0, pos(s(s(s(z1)))))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ QDP
CONDACC(false, z0, pos(s(s(z1)))) → SQRTACC(z0, pos(s(s(s(z1)))))
SQRTACC(z0, pos(s(s(s(z1))))) → CONDACC(or(greatereq_int(pos(plus_nat(plus_nat(plus_nat(mult_nat(z1, s(s(s(z1)))), s(s(s(z1)))), s(s(s(z1)))), s(s(s(z1))))), z0), false), z0, pos(s(s(s(z1)))))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
CONDACC(false, y0, neg(x1)) → SQRTACC(y0, minus_nat(s(0), x1))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
or(false, false) → false
or(true, false) → true
mult_nat(0, y) → 0
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
less_int(pos(0), pos(0)) → false
less_int(pos(s(x)), pos(0)) → false
or(false, true) → true
or(true, true) → true
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
CONDACC(false, y0, neg(x1)) → SQRTACC(y0, minus_nat(s(0), x1))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(true, false) → true
or(false, true) → true
or(true, true) → true
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
CONDACC(false, y0, neg(x1)) → SQRTACC(y0, minus_nat(s(0), x1))
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(true, false) → true
or(false, true) → true
or(true, true) → true
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
SQRTACC(y0, neg(s(x0))) → CONDACC(or(greatereq_int(pos(plus_nat(mult_nat(x0, s(x0)), s(x0))), y0), true), y0, neg(s(x0)))
Used ordering: Polynomial interpretation [POLO]:
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
CONDACC(false, y0, neg(x1)) → SQRTACC(y0, minus_nat(s(0), x1))
POL(0) = 1
POL(CONDACC(x1, x2, x3)) = x1
POL(SQRTACC(x1, x2)) = x2
POL(false) = 1
POL(greatereq_int(x1, x2)) = 0
POL(less_int(x1, x2)) = x1
POL(minus_nat(x1, x2)) = 1
POL(mult_nat(x1, x2)) = 0
POL(neg(x1)) = x1
POL(or(x1, x2)) = x2
POL(plus_nat(x1, x2)) = 0
POL(pos(x1)) = 0
POL(s(x1)) = 1
POL(true) = 0
or(true, false) → true
or(false, false) → false
less_int(neg(s(x)), pos(0)) → true
less_int(neg(0), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
or(false, true) → true
or(true, true) → true
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
CONDACC(false, y0, neg(x1)) → SQRTACC(y0, minus_nat(s(0), x1))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(true, false) → true
or(false, true) → true
or(true, true) → true
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CONDACC(false, y0, neg(x1)) → SQRTACC(y0, minus_nat(s(0), x1))
Used ordering: Polynomial interpretation [POLO]:
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
POL(0) = 1
POL(CONDACC(x1, x2, x3)) = x1
POL(SQRTACC(x1, x2)) = x2
POL(false) = 1
POL(greatereq_int(x1, x2)) = 0
POL(less_int(x1, x2)) = x1
POL(minus_nat(x1, x2)) = 0
POL(mult_nat(x1, x2)) = 1 + x1
POL(neg(x1)) = x1
POL(or(x1, x2)) = x2
POL(plus_nat(x1, x2)) = x2
POL(pos(x1)) = 0
POL(s(x1)) = 0
POL(true) = 0
or(true, false) → true
or(false, false) → false
less_int(neg(s(x)), pos(0)) → true
less_int(neg(0), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
or(false, true) → true
or(true, true) → true
↳ ITRS
↳ ITRStoQTRSProof
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ RemovalProof
↳ RemovalProof
↳ Narrowing
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Rewriting
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
SQRTACC(y0, neg(x0)) → CONDACC(or(greatereq_int(pos(mult_nat(x0, x0)), y0), less_int(neg(x0), pos(0))), y0, neg(x0))
mult_nat(s(x), s(y)) → plus_nat(mult_nat(x, s(y)), s(y))
mult_nat(0, y) → 0
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
less_int(neg(0), pos(0)) → false
less_int(neg(s(x)), pos(0)) → true
or(false, false) → false
or(true, false) → true
or(false, true) → true
or(true, true) → true
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
or(false, false)
or(false, true)
or(true, false)
or(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))
mult_nat(0, x0)
mult_nat(s(x0), 0)
mult_nat(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
less_int(pos(0), pos(0))
less_int(pos(0), neg(0))
less_int(neg(0), pos(0))
less_int(neg(0), neg(0))
less_int(pos(0), pos(s(x0)))
less_int(neg(0), pos(s(x0)))
less_int(pos(0), neg(s(x0)))
less_int(neg(0), neg(s(x0)))
less_int(pos(s(x0)), pos(0))
less_int(neg(s(x0)), pos(0))
less_int(pos(s(x0)), neg(0))
less_int(neg(s(x0)), neg(0))
less_int(pos(s(x0)), neg(s(x1)))
less_int(neg(s(x0)), pos(s(x1)))
less_int(pos(s(x0)), pos(s(x1)))
less_int(neg(s(x0)), neg(s(x1)))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))